single-thread-generator{i:l}(es;P;R)
== (e:E. Dec(P(e)))
== & (e, e':E. Dec(R(e',e)))
== & R => x,y. (x < y)
== & (e, e':E. (P(e) & R(e',e))  P(e'))
== & (m, m':E.
== & (P(m)  P(m')  (e:E. (e R m)  (P(e)))  (e:E. (e R m')  (P(e)))  (m = m'))
== & (a, b, e:E. (R(e,a) & R(e,b))  (P(e) & P(a) & P(b))  (a = b)) 

latex

---

clarification:

single-thread-generator{i:l}
single-thread-generator(es; P; R)
== (e:es-E(es). Dec(P(e)))
== & (e:es-E(es), e':es-E(es). Dec(R(e',e)))
== & rel_implies(es-E(es);R;x,y. es-causl(es; x; y))
== & (e:es-E(es), e':es-E(es). (P(e) & R(e',e))  P(e'))
== & (m:es-E(es), m':es-E(es).
== & (P(m)
== & ( P(m')
== & ( (e:es-E(es). (e R m)  (P(e)))
== & ( (e:es-E(es). (e R m')  (P(e)))
== & ( (m = m'  es-E(es)))
== & (a:es-E(es).
== & (b:es-E(es), e:es-E(es).
== & ((R(e,a) & R(e,b))  (P(e) & P(a) & P(b))  (a = b  es-E(es))) 

latex

Definitions	Dec(P), R1 => R2, x.A(x), (e < e'), x f y, A, x:A. B(x), f(a), P  Q, P & Q, x(s), s = t, E
FDL editor aliases	single-thread-generator